Step of Proof: last_member
11,40
postcript
pdf
Inference at
*
I
of proof for Lemma
last
member
:
T
:Type,
L
:(
T
List). (
(
null(
L
)))
(last(
L
)
L
)
latex
by ((((Unfolds ``l_member last`` 0)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C
),(first_nat 3:n)) (first_tok :t) inil_term)))
)
CollapseTHEN (Assert ||
L
|| > 0
THENL [((((
T
RW assert_pushdownC (-1))
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat
C
3:n)) (first_tok :t) inil_term)))
)
CollapseTHEN (Easy))
;
Colla
((InstConcl [||
L
|| - 1])
Co
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t
C
) inil_term)))
]))
latex
C
.
Definitions
False
,
A
B
,
t
T
,
,
i
>
j
,
A
c
B
,
,
x
:
A
.
B
(
x
)
,
last(
L
)
,
(
x
l
)
,
A
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
P
Q
Lemmas
null
wf
,
not
wf
,
select
wf
,
le
wf
,
length
wf1
,
non
nil
length
,
assert
of
null
,
assert
wf
,
not
functionality
wrt
iff
origin